http://shemesh.larc.nasa.gov/fm-top.html
NASA's Formal Methods Program is an attempt to implement a formal method in the design of safety-critical software and hardaware systems. The purpose of formal methods is to assure that even the mosty subtle design errors do not creep into life-critical systems such as the navigational system on NASA's Space Shuttle. Traditional methods of error detection such as thorough testing cannot provide the required 'ultra-high' degree of reliability with extremely complex systems, thus the application of formal methods to the design process. The web page offers users detailed descriptions of formal methods; projects that the program is working on; and the goals, facilities and staff. Users will also find a publically-accessible ftp directory containing material related to the application of formal methods, and a list of available publications.